perm filename FOUND.HLP[1,JRA] blob sn#005906 filedate 1972-09-28 generic text, type T, neo UTF8
00100	(ELEM(X3 X1) ≡ ELEM(X3 X2))⊃EQU(X1 X2);
00200	∀(X1 X2 )∃(X3)∀(X4)(ELEM(X4 X3) ≡(EQU(X4 X1) ∨ EQU(X4 X2)));
00300	∀(X1)(¬EMPTY(X1) ⊃ ∃(X2)(ELEM(X2 X1) ∧ DSJ(X2 X1)));
00400	∀(X1)(EMPTY(X1) ≡ ∀(X2)¬ELEM(X2 X1));
00500	∀(X1 X2)(DSJ(X1 X2) ≡ ∀(X3)¬(ELEM(X3 X1)∧ELEM(X3 X2)));
00600	;
00700	;
00800	¬ELEM(X1 X1);
00900	;